Ordered Binary Decision Diagrams (OBDDs) are widely used in design automation, primarily because of the ability of OBDD data structures to represent complex systems in a memory-efficient manner. Tools based on OBDD manipulation have been developed for use, inter alia, in automated formal verification of hardware circuits and other systems that can be represented as finite state machines. For example, U.S. patent application Ser. No. 10/042,304, published as U.S. 2002/0193974 A1, whose disclosure is incorporated herein by reference, describes a method for symbolic model checking based on OBDDs. The method is used to check a model (also referred to as an implementation) of a given hardware design against the design specification. The model is represented by an OBDD, which defines states of the system under study and a transition relation among the states. A reachability analysis is performed, using the OBDD, in order to find traces in the state space of the system that link an initial state to a target state having a specified property, which may either comply with or violate the specification.
Bryant and Meinel provide a useful review of the properties and applications of OBDDs in “Ordered Binary Decision Diagrams in Electronic Design Automation,” published in Logic Synthesis and Verification (Kluwer Academic Publishers, 2001), pages 285–307, which is incorporated herein by reference. To summarize briefly, an OBDD is a directed acyclic graph consisting of nonterminal nodes labeled by the variables in a set V and terminal nodes labeled by the Boolean constants 1 and 0. Each nonterminal node has two outgoing edges: a 1-edge and a 0-edge. The starting node of the ordered BDD is called the root.
A Boolean function f on the variables in V, for a given assignment of the values of the variables, is computed by following a path from the root to a terminal node. At each node along the path, if the corresponding variable x is assigned the value 1, the path follows the 1-edge. Otherwise, the path follows the 0-edge. Each variable occurs at most once on any given path. The value of the terminal node that is reached at the end of the path is the value of f for the given assignment. All paths from the root to either terminal node respect the variable ordering of the OBDD, i.e., if variable x occurs before variable y on one path in a given BDD ordering, then variable y will never occur before variable x on any other path. Therefore, the OBDD graph is typically “levelized,” so that all nodes corresponding to a given variable appear together in a row. The variable ordering of the OBDD can be altered, however, using simple logical techniques that are known in the art, without changing the underlying Boolean function that the OBDD represents.
The size of an OBDD (i.e., the number of nodes in the OBDD, and hence the complexity of its manipulation and memory consumption) depends strongly on the variable order. Therefore, in many OBDD applications, dynamic variable reordering is used to modify the variable order, and thus reduce the size, of the OBDD in the course of the application.
One commonly-used method for OBDD reordering is “sifting,” as described by Rudell in “Dynamic Variable Ordering for Ordered Binary Decision Diagrams,” Proceedings of the IEEE International Conference on Computer-Aided Design (Santa Clara, Calif., 1993), pages 42–47, which is incorporated herein by reference. Sifting makes use of the fact that swapping the order of two adjacent variables in the OBDD affects only the nodes of the OBDD in the corresponding rows of the graph. The sifting algorithm seeks an optimal position for a selected variable in the OBDD by swapping the corresponding row up and down over the entire graph while the positions of all other variables remain fixed. After the variable has traversed all possible positions, the optimal position is identified, and the variable is swapped back to that position. The procedure is then repeated to optimize the positions of other variables.
Other OBDD reordering methods attempt to perform variable reordering over a selected subset or block of the variables. For example Song and Chang describe what they call a “distributed reordering algorithm,” in “A Variable Reordering Method for Fast Optimization of Binary Decision Diagrams,” Proceedings of the Fifth Asian Test Symposium ATS'97 (IEEE, 1997), pages 228–233, which is incorporated herein by reference. The algorithm attempts to reduce optimization time by selecting a subset of the variables, which are not adjacent to one another, and exchanging the positions of the variables in the subset. As another example, Meinel and Slobodova describe a block-restricted sifting strategy in “Speeding Up Variable Reordering of OBDDs,” Proceedings of the International Conference on Computer Design (1997), pages 338–343, which is also incorporated herein by reference. This algorithm uses Rudell's sifting method, but restricts it to certain selected blocks of variables.